(set-logic QF_BV)
(declare-fun x0 () (_ BitVec 32))
(declare-fun x1 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun x3 () (_ BitVec 32))
(declare-fun x4 () (_ BitVec 32))
(declare-fun x5 () (_ BitVec 32))
(declare-fun x6 () (_ BitVec 32))
(assert 
  (let ((e9 (bvadd x1 x4))) 
  (let ((e11 (bvneg e9))) 
  (let ((e13 (bvnand e11 e11))) 
  (let ((e15 (bvnand x3 e9))) 
  (let ((e17 (bvsub (_ bv0 32) e15))) 
  (let ((e31 (bvmul e13 x2))) 
  (let ((e39 (bvsub x5 e13))) 
  (let ((e42 (bvand x0 e31))) 
  (let ((e46 (bvneg e13))) 
  (let ((e60 (ite (bvult e46 x6) (_ bv1 1) (_ bv0 1)))) 
  (let ((e211 (bvslt e42 (_ bv0 32)))) 
  (let ((e424 (distinct ((_ zero_extend 16) e60) (_ bv0 17)))) 
  (let ((e506 (=> true e424))) 
  (let ((e552 e211)) 
  (let ((e591 e506)) 
  (let ((e690 e591)) 
  (let ((e692 (= e552 false))) 
  (let ((e703 (= e692 true))) 
  (let ((e726 (not e703))) 
  (let ((e738 (=> e726 false))) 
  (let ((e772 (not e690))) 
  (let ((e789 (= e772 false))) 
  (let ((e792 (=> e738 false))) 
  (let ((e795 (xor e789 e792))) 
  (let ((e801 (= e795 false))) 
  (let ((e805 (xor e801 false))) 
  (let ((e813 e805)) 
  (let ((e817 (xor false e813))) 
  (let ((e819 (= false e817))) 
  (let ((e820 e819)) 
  (let ((e821 (and e820 (not (= e39 (_ bv0 32)))))) 
  (let ((e822 e821)) 
  (let ((e823 e822)) 
  (let ((e824 e823)) 
  (let ((e825 e824)) 
  (let ((e826 e825)) 
  (let ((e827 (and e826 (not (= e17 (_ bv0 32)))))) e827))))))))))))))))))))))))))))))))))))))
(check-sat)
